A, C, B:Type, eqa:EqDecider(A), eqc, eqc':EqDecider(C), r:(AC), f:a:A fp B, a:A, z:B.
Inj(A;C;r)  (rename(r;f)(r(a))?z = f(a)?z  B) 

latex

Definitions	x:A. B(x), P  Q, f(x)?z, if b then t else f fi , t  T, tt, x. t(x), ff, , x:A. B(x), A c B, , Unit, P  Q, P & Q, x(s), {T}, A, False, Inj(A;B;f), P  Q,
Lemmas	bool wf, eqtt to assert, fpf-dom wf, fpf-trivial-subtype-top, fpf-rename-ap2, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, inject wf, fpf wf, deq wf, fpf-rename wf, top wf, fpf-dom functionality2, fpf-rename-dom